((v7 v5 0) (v3 v8 3) (v2 v7 0) (v3 v6 3) (v5 v8 1) (v2 v6 6) (v6 v8 8) (v5 v2 8) (v2 v3 9) (v1 v6 1) (v2 v4 8) (v4 v1 9) (v8 v2 0) (v3 v5 9) (v3 v4 3) (v7 v6 3) (v8 v1 7) (v2 v1 8))
48
((v3 v7))